(set-option :produce-unsat-model-interpolants true)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(assert (let ((e1 10429464))
(let ((e2 94624804))
(let ((e3 (- v0)))
(let ((e4 (- v0 e3)))
(let ((e5 (- e4)))
(let ((e6 (* e5 e4)))
(let ((e7 (- e5)))
(let ((e8 (- e6)))
(let ((e9 (- e6)))
(let ((e10 (/ e1 e2)))
(let ((e11 (>= e3 e6)))
(let ((e12 (<= e3 e4)))
(let ((e13 (< e5 e5)))
(let ((e14 (>= e10 e3)))
(let ((e15 (<= e9 e8)))
(let ((e16 (>= e7 e6)))
(let ((e17 (< e5 v0)))
(let ((e18 (ite e15 e9 v0)))
(let ((e19 (ite e14 e8 v0)))
(let ((e20 (ite e11 e10 e3)))
(let ((e21 (ite e15 e7 e8)))
(let ((e22 (ite e15 e18 e19)))
(let ((e23 (ite e17 e6 e7)))
(let ((e24 (ite e15 e4 e5)))
(let ((e25 (ite e13 e23 e23)))
(let ((e26 (ite e15 e6 e7)))
(let ((e27 (ite e16 e7 e5)))
(let ((e28 (ite e12 e25 e18)))
(let ((e29 (> e6 e8)))
(let ((e30 (<= e24 e6)))
(let ((e31 (> e4 e10)))
(let ((e32 (= e5 e24)))
(let ((e33 (< e10 e21)))
(let ((e34 (< e8 e22)))
(let ((e35 (<= e18 v0)))
(let ((e36 (= e10 e18)))
(let ((e37 (>= e20 e22)))
(let ((e38 (<= e25 e5)))
(let ((e39 (>= e6 e22)))
(let ((e40 (distinct e21 e3)))
(let ((e41 (= e20 e18)))
(let ((e42 (> e7 e5)))
(let ((e43 (> e21 e4)))
(let ((e44 (>= e24 e10)))
(let ((e45 (<= e4 e8)))
(let ((e46 (distinct e10 e5)))
(let ((e47 (>= e22 e9)))
(let ((e48 (= e28 e7)))
(let ((e49 (< e9 e23)))
(let ((e50 (>= e4 e7)))
(let ((e51 (>= e27 e7)))
(let ((e52 (< e21 e23)))
(let ((e53 (> e4 e9)))
(let ((e54 (distinct e3 e21)))
(let ((e55 (= e5 e7)))
(let ((e56 (>= e3 e9)))
(let ((e57 (distinct e4 e19)))
(let ((e58 (= e6 e3)))
(let ((e59 (> e25 e3)))
(let ((e60 (<= e5 e5)))
(let ((e61 (distinct e3 v0)))
(let ((e62 (= e21 e23)))
(let ((e63 (distinct e25 e20)))
(let ((e64 (>= e21 e4)))
(let ((e65 (> e5 e7)))
(let ((e66 (< e4 e19)))
(let ((e67 (< e9 e20)))
(let ((e68 (>= e6 e25)))
(let ((e69 (distinct e5 e20)))
(let ((e70 (= e7 e5)))
(let ((e71 (distinct e8 e21)))
(let ((e72 (< e20 e10)))
(let ((e73 (= v0 e9)))
(let ((e74 (>= v0 e18)))
(let ((e75 (>= e22 e4)))
(let ((e76 (<= e8 e19)))
(let ((e77 (> e21 e9)))
(let ((e78 (distinct v0 e18)))
(let ((e79 (< e27 e28)))
(let ((e80 (= e20 e21)))
(let ((e81 (>= e10 e18)))
(let ((e82 (= e21 e5)))
(let ((e83 (> e22 e25)))
(let ((e84 (> e26 e25)))
(let ((e85 (= e49 e55)))
(let ((e86 (or e46 e76)))
(let ((e87 (or e70 e78)))
(let ((e88 (or e32 e60)))
(let ((e89 (ite e30 e37 e16)))
(let ((e90 (= e68 e51)))
(let ((e91 (or e41 e11)))
(let ((e92 (and e66 e29)))
(let ((e93 (= e81 e64)))
(let ((e94 (= e67 e91)))
(let ((e95 (= e79 e39)))
(let ((e96 (xor e35 e58)))
(let ((e97 (or e47 e50)))
(let ((e98 (=> e12 e13)))
(let ((e99 (= e14 e62)))
(let ((e100 (xor e31 e15)))
(let ((e101 (ite e40 e87 e34)))
(let ((e102 (and e80 e99)))
(let ((e103 (=> e94 e63)))
(let ((e104 (xor e17 e98)))
(let ((e105 (=> e71 e36)))
(let ((e106 (ite e82 e59 e53)))
(let ((e107 (and e89 e61)))
(let ((e108 (ite e72 e69 e100)))
(let ((e109 (= e52 e95)))
(let ((e110 (=> e97 e73)))
(let ((e111 (or e43 e88)))
(let ((e112 (or e57 e101)))
(let ((e113 (and e110 e56)))
(let ((e114 (or e113 e77)))
(let ((e115 (not e111)))
(let ((e116 (not e45)))
(let ((e117 (and e109 e116)))
(let ((e118 (= e44 e74)))
(let ((e119 (=> e112 e107)))
(let ((e120 (not e118)))
(let ((e121 (not e93)))
(let ((e122 (= e65 e104)))
(let ((e123 (and e85 e38)))
(let ((e124 (=> e102 e102)))
(let ((e125 (or e48 e115)))
(let ((e126 (= e106 e86)))
(let ((e127 (=> e96 e120)))
(let ((e128 (=> e124 e108)))
(let ((e129 (ite e103 e75 e114)))
(let ((e130 (not e54)))
(let ((e131 (and e126 e105)))
(let ((e132 (not e123)))
(let ((e133 (not e132)))
(let ((e134 (xor e42 e127)))
(let ((e135 (not e125)))
(let ((e136 (=> e128 e119)))
(let ((e137 (and e129 e135)))
(let ((e138 (= e133 e136)))
(let ((e139 (not e121)))
(let ((e140 (ite e84 e138 e83)))
(let ((e141 (or e131 e33)))
(let ((e142 (ite e122 e141 e117)))
(let ((e143 (not e140)))
(let ((e144 (or e137 e92)))
(let ((e145 (xor e139 e139)))
(let ((e146 (and e90 e134)))
(let ((e147 (not e144)))
(let ((e148 (= e130 e147)))
(let ((e149 (= e146 e148)))
(let ((e150 (or e143 e143)))
(let ((e151 (= e142 e145)))
(let ((e152 (= e151 e149)))
(let ((e153 (or e152 e152)))
(let ((e154 (not e150)))
(let ((e155 (= e153 e153)))
(let ((e156 (= e155 e155)))
(let ((e157 (not e156)))
(let ((e158 (not e154)))
(let ((e159 (xor e158 e157)))
e159
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat-assuming-model (v0) ((/ 94 (- 51))))
(get-unsat-model-interpolant)
